p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))
↳ QTRS
↳ DependencyPairsProof
p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))
P(a(x0), p(a(b(x1)), x2)) → P(a(a(x1)), x2)
P(a(x0), p(a(b(x1)), x2)) → P(a(b(a(x2))), p(a(a(x1)), x2))
p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
P(a(x0), p(a(b(x1)), x2)) → P(a(a(x1)), x2)
P(a(x0), p(a(b(x1)), x2)) → P(a(b(a(x2))), p(a(a(x1)), x2))
p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(a(x0), p(a(b(x1)), x2)) → P(a(a(x1)), x2)
Used ordering: Combined order from the following AFS and order.
P(a(x0), p(a(b(x1)), x2)) → P(a(b(a(x2))), p(a(a(x1)), x2))
P1 > [a1, p1, b]
b: multiset
a1: [1]
P1: multiset
p1: [1]
p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
P(a(x0), p(a(b(x1)), x2)) → P(a(b(a(x2))), p(a(a(x1)), x2))
p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(a(x0), p(a(b(x1)), x2)) → P(a(b(a(x2))), p(a(a(x1)), x2))
[p2, b1]
b1: multiset
p2: multiset
p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))